copilot-theorem: Translate quantifiers correctly in Kind2 backend. Refs #594. - #610

Change Manager: Please see the comments above regarding alignment.

Implementor: Fix implemented, review requested.

Change Manager: Please rebase branch wrt. the latest master.

Implementor: Fix implemented, review requested.

Change Manager: Verified that:

• Solution is implemented:
  • The code proposed compiles and passes all tests. Details:
    Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/274932248
  • The solution proposed produces the expected result. Details:
    The following Dockerfile uses the kind2 backend to Copilot spec to try to prove a universal and an existential property, and checks that the result reported by copilot-theorem matches the expectation, after which it prints the message "Success":

    --- Dockerfile-verify-594
    FROM ubuntu:focal
    
    RUN apt-get update
    
    RUN apt-get install --yes software-properties-common
    RUN add-apt-repository ppa:hvr/ghc
    RUN apt-get update
    
    RUN apt-get install --yes \
      ghc-8.6.5 cabal-install-2.4 \
      libtool-bin libz-dev libzmq5 opam z3
    
    # Install Kind2's OCaml dependencies
    RUN opam init --auto-setup --yes --bare --disable-sandboxing \
     && opam switch create default 4.01.0 \
     && opam repository add archive git+https://github.com/ocaml/opam-repository-archive \
     && opam install -y -j "$(nproc)" camlp4 menhir \
     && opam clean -a -c -s --logs
    
    # Install Kind2-0.7.2
    ENV KIND2_VER="0.7.2"
    RUN wget https://github.com/kind2-mc/kind2/archive/refs/tags/v${KIND2_VER}.zip \
     && unzip v${KIND2_VER}.zip
    WORKDIR kind2-${KIND2_VER}
    RUN sed -i.bak -e 's/-pedantic -Werror -Wall/-pedantic -Wall/' ocamlczmq/czmq/configure.ac
    RUN eval $(opam env) \
     && ./autogen.sh \
     && ./build.sh \
     && make install
    WORKDIR /
    
    # Install GHC and Cabal
    ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH
    
    RUN cabal update
    RUN cabal v1-sandbox init
    RUN apt-get install --yes git
    
    ADD Spec.hs /tmp/Spec.hs
    
    SHELL ["/bin/bash", "-c"]
    CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
      && cabal v1-install alex happy \
      && cabal v1-install $NAME/copilot**/ \
      && (cabal v1-exec -- runhaskell /tmp/Spec.hs | grep -e "t1: proof failed" -e "t2: proof checked successfully") \
      && echo "Success"
    
    --- Spec.hs
    {-# LANGUAGE NoImplicitPrelude #-}
    module Main (main) where
    
    import Data.Functor
    
    import Copilot.Theorem.Kind2
    import Copilot.Theorem.Prove
    import Language.Copilot
    
    trueThenFalses :: Stream Bool
    trueThenFalses = [True] ++ constant False
    
    spec :: Spec
    spec = do
      void $ theorem "t1" (forAll trueThenFalses) (check (kind2Prover def))
      void $ theorem "t2" (exists trueThenFalses) (check (kind2Prover def))
    
    main :: IO ()
    main = void $ reify spec
    

    Command (substitute variables based on new path after merge):

    $ docker run -e REPO=https://github.com/GaloisInc/copilot-1 -e NAME=copilot-1 -e COMMIT=3b51c969d863755431cb628de80bc02e0c243a8d copilot-verify-594
    

• Implementation is documented. Details:
  The code is documented and changes to top-level definitions are adjusted where needed.
• Change history is clear.
• Commit messages are clear.
• Changelogs are updated.
• Examples are updated. Details:
  No updates needed.
• Required version bumps are evaluated. Details:
  Bump not required; change fixes a bug but does not affect public API.